The advancement of network technologies such as bluetooth and WiFi has promoted the development of the Internet of Things(IoT). IoT facilitates people's lives, but there are also serious security issues in it. Without secure access control, illegal access of IoT may bring losses to users in many aspects. Traditional access control methods usually rely on a trusted central node, which is not suitable for an IoT environment with nodes distributed. The blockchain technology and smart contracts provide a more effective solution for access control in IoT applications. However, it is difficult to ensure the correctness of smart contracts used for access control in IoT applications by using general test methods. To solve this problem, a method was proposed to formally verify the correctness of smart contracts for access control by using model checking tool Verds. In the method, the state transition system was used to define the semantics of the Solidity smart contract, the Computation Tree Logic(CTL) formula was used to describe the properties to be verified, and the smart contract interaction and user behavior were modelled to form the input model of Verds and the properties to be verified. And then Verds was used to verify whether the properties to be verified are correct. The core of this method is the translation from a subset of Solidity to the input model of Verds. Experimental results on two smart contracts for access control of IoT source show that the proposed method can be used to verify some typical scenarios and expected properties of access control contracts, thereby improving the reliability of smart contracts.

Focusing on the problem whether there are new security flaws of several kinds of high-level cryptographic S-boxes, an algorithm for solving the nonlinear invariant function of S-boxes was proposed, which is mainly based on the algebraic relationship between the input and output of the cryptographic S-boxes. Using the proposed algorithm, several kinds of S-boxes were tested and it was found that several of them had the same nonlinear invariant function. In addition, if these S-boxes were used to non-linear parts of the block cipher Midori-64, a new variant algorithm would be obtained. The security analysis was carried out by non-linear invariant attack. The analytical results show that the Midori-64 variant is faced with serious secure vulnerability. In other words, there exist 2 ⁶⁴ weak keys when nonlinear invariant attack is applied to the Midori-64 variant, meanwhile data, time and storage complexity can be neglected, consequently some high-level cryptographic S-boxes have security flaws.

With the growing richness of modern network security devices, network security logs show a trend of multiple heterogeneity. In order to solve the problem of large-scale, heterogeneous, rapid changing network logs, a visual method was proposed for fusing network security logs and understanding network security situation. Firstly, according to the eight selected characteristics of heterogeneous security logs, information entropy, weighted method and statistical method were used respectively to pre-process network characteristics. Secondly, treemap and glyph were used to dig into the security details from micro level, and time-series chart was used to show the development trend of the network from macro level. Finally, the system also created graphical features to visually analyze network attack patterns. By analyzing network security datasets from VAST Challenge 2013, the experimental results show substantial advantages of this proposal in understanding network security situation, identifying anomalies, discovering attack patterns and removing false positives, etc.

Otsu has been widely used because of its simplicity in calculation and good segmentation result. And many scholars have put forward multi-threshold Otsu method to make it more useful in more complex pictures. But this multi-threshold Otsu method is of low efficiency and time consuming. Concerning this shortage, this paper made histogram intervals first, and then the rapid dichotomy was used to seek for the threshold in the interval. The improvement in this paper can maintain good segmentation result and save lots of time. The experiments show that the algorithm is effective.